w:World, e:E.
FairFifo
 rcv?(e)
 (msg(lnk(kind(e));tag(kind(e));val(e))  m(loc(sender(e));time(sender(e)))) 

latex

Definitions

t  T, act(e), kind(e), loc(e), x:A. B(x), E, P  Q, Id, World, FairFifo, rcv?(e), w.M, Msg(M), (x  l), w-info(w;e), x.A(x), kind(e), isrcv(k), b, sender(e), time(e), False, True, tag(k), lnk(k), act(k), islocal(k), kindcase(k; a.f(a); l,t.g(l;t) ), x:AB(x), left+right, Knd, x:AB(x), s = t, {x:A| B(x) }, ecase1(e;info;i.f(i);l,e'.g(l;e')), link(e), a(i;t), kind(a), msg(a), val(e), msg(l;t;v), s ~ t, P & Q, source(l), mlnk(m), type List, S  T, m(i;t), a = b, P  Q, Msg, onlnk(l;mss), P  Q, A, AB, , , outl(x), 1of(t), IdLnk, T, SqStable(P), , b, Prop, Unit, Void, isrcv(l;a), isnull(a), <a,b>, loc(e), {T}, SQType(T)

Lemmas

Id sq, w-loc-sender, w-isnull wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, isrcv wf, bool wf, sq stable from decidable, decidable assert, assert-eq-lnk, w-msg wf, w-loc wf, member filter, eq lnk wf, w-m wf, Msg wf, mlnk wf, w-M wf, lsrc wf, lnk wf, w-ekind wf, w-kind wf, w-a wf, Knd wf, true wf, false wf, assert wf, rcv? wf, fair-fifo wf, world wf, w-match-sender, w-match-member-property, w-time wf, sender wf, rcv?-kind, Id wf, w-info wf, w-E wf, w-kind-lemma